mcsta/modest mcsta dpm.jani -E N=4,C=8,TIME_BOUND=5 --props PmaxQueuesFullBound -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --width 5e-2 --relative-width
dpm.jani:model: info: dpm is an MA model.
dpm.jani: info: Need 16 bytes per state.
dpm.jani: info: Explored 356426 states for N=4, C=8, TIME_BOUND=5.0.
dpm.jani: info: Identified 356417 maximal end components.
Peak memory usage: 190 MB
Analysis results for dpm.jani
Experiment N=4, C=8, TIME_BOUND=5.0
+ State space exploration
State size: 16 bytes
States: 356426
Transitions: 418842
Branches: 681242
Rate: 424822 states/s
Time: 0.9 s
+ Property PmaxQueuesFullBound
Probability: 2.247385514171146E-08
Bounds: [2.2273443135310677E-08, 2.267426714811224E-08]
Time: 6.1 s
+ Precomputations
Max. prob. 0 states: 0
Time for max. prob. 0 states: 0.0 s
+ End components
Iterations: 2
MECs: 356417
Transitions: 418833
Branches: 681233
Time: 0.3 s
+ Essential states
Iterations: 2
Essential states: 123138
Transitions: 185554
Branches: 447954
Time: 0.1 s
+ Unif+
Time: 5.7 s
Max. exit rate: 4.1
Iterations: 2
Final unif. rate: 4.1
Exported results to file "/out.txt".